(* this is an -*- sml -*- file *)

(* ======================================================================
       Automatic generation of clickable image maps of the
       HOL theory hierarchy.
   ----------------------------------------------------------------------

    The algorithm works as follows:

      1. Generate the dependencies from the current theory hierarchy
      2. Write them to a file ready for processing by "dot"
      3. Invoke dot to generate the SVG image
      4. Generate a HTML file to hold the reference to the image
      5. Generate the html files for each segment in the current
         theory hierarchy.

    Before loading this file, you might need to tell "dot" where the
    TrueType fonts that it needs are. On my Linux system, this used to
    be:

        DOTFONTPATH=/dosc/windows/fonts; export DOTFONTPATH

    Run the file by

       hol < DOT

   ====================================================================== *)

val _ = HOL_Interactive.toggle_quietdec();

fun die s =
  (TextIO.output(TextIO.stdErr, s ^ "\n");
   TextIO.flushOut TextIO.stdErr;
   OS.Process.exit OS.Process.failure)

val HTML_DIR   = Path.toString(Path.fromString(Path.concat
                    (Globals.HOLDIR,"help/theorygraph")));
val SIGOBJ_DIR = Path.toString(Path.fromString(Path.concat
                    (Globals.HOLDIR,"sigobj")));

val DOTPATH =
    case Systeml.DOT_PATH of
        NONE => die "No DOT_PATH in Systeml"
      | SOME s => s

(*---------------------------------------------------------------------------
     Extract dot-friendly digraph from HOL theory graph.
 ---------------------------------------------------------------------------*)

fun node thy = map (fn p => (p,thy)) (parents thy);

local fun leq (s:string,_) (t,_) = s <= t
in
fun ancestor_nodes thy =
  let val thys = ancestry thy
      val pairs = sort leq (flatten (map node thys))
  in (thys, pairs)
  end
end;

(*---------------------------------------------------------------------------*)
(* There are lots of parameters that can be played with here. See the dot    *)
(* manual for tweakables.                                                    *)
(*---------------------------------------------------------------------------*)

fun pp_dot_file {size,ranksep,nodesep} (dom,pairs) =
 let open Portable PP
     fun pp_thy s =
       block CONSISTENT 2 [
        add_string s, add_break (1,0),
        add_string "[URL =", add_break(1,0),
        add_string (quote (s^"Theory.html")),
        add_string "]"
       ]
     fun pp_pair (x,y) =
       block CONSISTENT 0 [add_string x, add_string " -> ", add_string y]
 in
   block CONSISTENT 0 [
     block CONSISTENT 5 [
       add_string "digraph G {",
       add_break (1,0),
       add_string "bgcolor = transparent", add_break(1,0),
       add_string "ratio = compress", add_break(1,0),
       add_string "size = ",    add_string (quote size), add_break(1,0),
       add_string "ranksep = ", add_string ranksep,      add_break(1,0),
       add_string "nodesep = ", add_string nodesep,      add_break(1,0),
       add_string "node [target=_parent style=filled fillcolor=white fontcolor=darkgreen fontsize=30 fontname=Arial]",
       add_break(1,0),
       add_newline,
       block CONSISTENT 0 (pr_list pp_thy [add_newline] dom),
       add_newline, add_newline,
       block CONSISTENT 0 (pr_list pp_pair [add_newline] pairs)
     ],
     add_newline, add_string "}", add_newline
   ]
 end;

fun gen_dotfile file node_info =
 let open TextIO
     val ostrm = openOut file
 in
   PP.prettyPrint(curry output ostrm, 75)
                 (pp_dot_file {size="16,16",ranksep="1.0",nodesep="0.30"}
                              node_info);
   closeOut ostrm
 end;

(* ----------------------------------------------------------------------
    cat filename out

    push contents of filename into outstream out
   ---------------------------------------------------------------------- *)

fun cat fname outstr = let
  val instr = TextIO.openIn fname
  val infile = TextIO.inputAll instr
in
  TextIO.output(outstr, infile)
end

(*---------------------------------------------------------------------------
       Parse theory coordinates generated by dot -Timap. Note that
       these come (i,j) (p,q), but it seems that they should be
       transformed to (i,q) (p,j) ... and so that's what we do!
 ---------------------------------------------------------------------------*)

fun gen_map_file dot node_info name = let
  open TextIO
  val dotfile   = name^".dot"
  val svgfile   = name^".svg"
  val mapfile   = name^".html"
  val  _        = gen_dotfile dotfile node_info
  val cmdstatus = Systeml.systeml [dot,
                                   "-Tsvg", "-o"^svgfile,
                                   dotfile]
in
  if OS.Process.isSuccess cmdstatus then let
      val _ = print "Called dot successfully.\n"
      val ostrm = openOut mapfile
      fun out s = output(ostrm, s^"\n")
    in
      out "<!DOCTYPE html>";
      out "<HTML>";
      out "<META CHARSET=\"utf-8\">";
      out "<HEAD><TITLE>HOL Theory Hierarchy</TITLE></HEAD>";
      out "<BODY bgcolor=linen>";
      out "<H1>HOL Theory Hierarchy (clickable)</H1>";
      out (String.concat
               ["<object data=\"",OS.Path.file svgfile,"\" type=\"image/svg+xml\">HOL Theory Map</object>"]);
      out "</BODY>";
      out "</HTML>";
      closeOut ostrm
    end
  else raise Fail "gen_map_file: failed "
end;

fun dir_theories dir = let
  open Substring FileSys
  val dstrm = openDir dir
  fun thys () =
      case readDir dstrm of
        NONE => []
      | SOME file => let
          val (ss1,ss2) = position "Theory.sig" (full file)
        in
          if isEmpty ss1 orelse isEmpty ss2 orelse string ss1 = "Final" then
            thys()
          else string ss1 :: thys()
        end
in
  thys()
end;


val load_theories = let
  fun loadi i s = (if i mod 5 = 0 then print "." else () ;
                   load (s^"Theory"))
in
  appi loadi
end

fun pappi f (l1,l2) = let
  fun recurse i (l1,l2) =
      case (l1,l2) of
        ([], _) => ()
      | (_, []) => ()
      | (h1::t1,h2::t2) => (f i (h1,h2) ; recurse (i + 1) (t1, t2))
in
  recurse 0 (l1,l2)
end

(* ----------------------------------------------------------------------
    Up to this point, no work is done - the above just sets up
    functions to do the work.  What follows actually figures out what
    the graph is and causes lots of stuff to be written to disk
   ---------------------------------------------------------------------- *)

val sys_theories = List.filter (not o String.isSuffix "_emit")
                               (dir_theories SIGOBJ_DIR);
(* trailing spaces make this line up with HTML printing message later *)
val _ = print "\n\nLoading system theories        ";
load_theories sys_theories;
val _ = print " done\n"
val ancs = ancestor_nodes "-";

val all_theories = "min"::sys_theories;
val paths = map(fn s => Path.concat (HTML_DIR,s^"Theory.html")) all_theories;
val _ = print "Printing HTML theories to disk ";
fun appthis i (thy,path) =
    (if i mod 5 = 0 then print "." else ();
     print_theory_as_html thy path
     handle Fail s => print (">>> PP failure on "^thy^": "^s^"\n"))
val _ = pappi appthis (all_theories, paths);
val _ = print " done\n";

(* The following works on Unix with dot version 1.10.2003xxxxxxx *)

gen_map_file DOTPATH ancs (Path.concat(HTML_DIR, "theories"))
    handle _ =>
      die ("Failed to call gen_map_file on dot="^DOTPATH^" targeting "^
           Path.concat(HTML_DIR, "theories"))
;
